Process completed with exit code 1.

Non-empty-diff: diff --git a/fiat-bedrock2/src/curve25519_32.c b/fiat-bedrock2/src/curve25519_32.c index d525c33..f274e72 100644 --- a/fiat-bedrock2/src/curve25519_32.c +++ b/fiat-bedrock2/src/curve25519_32.c @@ -806,7 +806,6 @@ void internal_fiat_25519_carry_mul(br_word_t out0, br_word_t in0, br_word_t in1) _br_store(out0+32, x667); _br_store(out0+36, x668); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -1287,7 +1286,6 @@ void internal_fiat_25519_carry_square(br_word_t out0, br_word_t in0) { _br_store(out0+32, x447); _br_store(out0+36, x448); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -1361,7 +1359,6 @@ void internal_fiat_25519_carry(br_word_t out0, br_word_t in0) { _br_store(out0+32, x40); _br_store(out0+36, x41); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -1435,7 +1432,6 @@ void internal_fiat_25519_add(br_word_t out0, br_word_t in0, br_word_t in1) { _br_store(out0+32, x38); _br_store(out0+36, x39); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -1509,7 +1505,6 @@ void internal_fiat_25519_sub(br_word_t out0, br_word_t in0, br_word_t in1) { _br_store(out0+32, x38); _br_store(out0+36, x39); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -1571,7 +1566,6 @@ void internal_fiat_25519_opp(br_word_t out0, br_word_t in0) { _br_store(out0+32, x28); _br_store(out0+36, x29); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -1667,7 +1661,6 @@ void internal_fiat_25519_selectznz(br_word_t out0, br_word_t in0, br_word_t in1, _br_store(out0+32, x58); _br_store(out0+36, x59); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -1970,7 +1963,6 @@ void internal_fiat_25519_to_bytes(br_word_t out0, br_word_t in0) { _br_store1(out0+30, x247); _br_store1(out0+31, x248); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -2122,7 +2114,6 @@ void internal_fiat_25519_from_bytes(br_word_t out0, br_word_t in0) { _br_store(out0+32, x118); _br_store(out0+36, x119); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -2184,7 +2175,6 @@ void internal_fiat_25519_relax(br_word_t out0, br_word_t in0) { _br_store(out0+32, x28); _br_store(out0+36, x29); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -2311,7 +2301,6 @@ void internal_fiat_25519_carry_scmul_121666(br_word_t out0, br_word_t in0) { _br_store(out0+32, x93); _br_store(out0+36, x94); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ diff --git a/fiat-bedrock2/src/curve25519_64.c b/fiat-bedrock2/src/curve25519_64.c index c20f57c..ccdf47c 100644 --- a/fiat-bedrock2/src/curve25519_64.c +++ b/fiat-bedrock2/src/curve25519_64.c @@ -307,7 +307,6 @@ void internal_fiat_25519_carry_mul(br_word_t out0, br_word_t in0, br_word_t in1) _br_store(out0+24, x173); _br_store(out0+32, x174); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -452,7 +451,6 @@ void internal_fiat_25519_carry_square(br_word_t out0, br_word_t in0) { _br_store(out0+24, x116); _br_store(out0+32, x117); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -501,7 +499,6 @@ void internal_fiat_25519_carry(br_word_t out0, br_word_t in0) { _br_store(out0+24, x20); _br_store(out0+32, x21); /*skip*/ - return; } /* NOTE: The following wrapper function is not covered by Coq proofs */ @@ -550,7 +547,6 @@ void internal_fiat_25519_add(br_word_t out0, br_word_t in0, br_word_t in1) { _br_store(out0+24, x18); _br_store(out0+32, x19); /*skip*/ - return;

Process completed with exit code 1.

Unexpected input(s) 'tags', valid inputs are ['repository', 'ref', 'token', 'ssh-key', 'ssh-known-hosts', 'ssh-strict', 'ssh-user', 'persist-credentials', 'path', 'clean', 'filter', 'sparse-checkout', 'sparse-checkout-cone-mode', 'fetch-depth', 'fetch-tags', 'show-progress', 'lfs', 'submodules', 'set-safe-directory', 'github-server-url']

Unexpected input(s) 'tags', valid inputs are ['repository', 'ref', 'token', 'ssh-key', 'ssh-known-hosts', 'ssh-strict', 'ssh-user', 'persist-credentials', 'path', 'clean', 'filter', 'sparse-checkout', 'sparse-checkout-cone-mode', 'fetch-depth', 'fetch-tags', 'show-progress', 'lfs', 'submodules', 'set-safe-directory', 'github-server-url']

Unexpected input(s) 'tags', valid inputs are ['repository', 'ref', 'token', 'ssh-key', 'ssh-known-hosts', 'ssh-strict', 'ssh-user', 'persist-credentials', 'path', 'clean', 'filter', 'sparse-checkout', 'sparse-checkout-cone-mode', 'fetch-depth', 'fetch-tags', 'show-progress', 'lfs', 'submodules', 'set-safe-directory', 'github-server-url']