projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c77213e) | patch
[LFSC] Fix segfault
authorAndres Notzli <andres.noetzli@gmail.com>
Sun, 26 Mar 2017 21:39:07 +0000 (23:39 +0200)
committerAndres Notzli <andres.noetzli@gmail.com>
Wed, 5 Apr 2017 14:45:40 +0000 (07:45 -0700)
commit90076eaba27567f7641751a65f0f784ffca317c4
tree7beda4cc71f18d12d402682605d3f715f260321ctree
parentc77213eaf165746a3704204ce56915b86c5f2a7acommit | 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.
proofs/lfsc_checker/code.cpp diff | blob | history
proofs/signatures/th_bv_bitblast.plf diff | blob | history