diff options
| author | Andres Notzli <andres.noetzli@gmail.com> | 2017-03-26 23:39:07 +0200 |
|---|---|---|
| committer | Andres Notzli <andres.noetzli@gmail.com> | 2017-04-05 07:45:40 -0700 |
| commit | 90076eaba27567f7641751a65f0f784ffca317c4 (patch) | |
| tree | 7beda4cc71f18d12d402682605d3f715f260321c /proofs/signatures | |
| parent | c77213eaf165746a3704204ce56915b86c5f2a7a (diff) | |
[LFSC] Fix segfault
LFSC did not detect when the number of arguments provided to a side
condition did not match the expected number of arguments, which could
lead to out-of-bounds reads and writes. This commit adds a check and
fixes one of the proof rules that provided the wrong number of
arguments.
Diffstat (limited to 'proofs/signatures')
| -rw-r--r-- | proofs/signatures/th_bv_bitblast.plf | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf index 2b2fe0868..109155a21 100644 --- a/proofs/signatures/th_bv_bitblast.plf +++ b/proofs/signatures/th_bv_bitblast.plf @@ -173,7 +173,7 @@ (! xb bblt (! rb bblt (! xbb (bblast_term m x xb) - (! c ( ^ (bblast_sextend xb k m) rb) + (! c ( ^ (bblast_sextend xb k) rb) (bblast_term n (sign_extend n k m x) rb)))))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |