diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/lfsc_checker/code.cpp | 19 | ||||
| -rw-r--r-- | proofs/signatures/th_bv_bitblast.plf | 2 |
2 files changed, 20 insertions, 1 deletions
diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp index ee143a710..48ebc5578 100644 --- a/proofs/lfsc_checker/code.cpp +++ b/proofs/lfsc_checker/code.cpp @@ -1303,7 +1303,9 @@ Expr *run_code(Expr *_e) { return tmp; } + assert(hd->getclass() == CEXPR); CExpr *prog = (CExpr *)hd; + assert(prog->kids[1]->getclass() == CEXPR); Expr **cur = ((CExpr *)prog->kids[1])->kids; vector<Expr *> old_vals; SymExpr *var; @@ -1331,10 +1333,26 @@ Expr *run_code(Expr *_e) { else { while((var = (SymExpr *)*cur++)) { + // Check whether not enough arguments were supplied + if (i >= args.size()) { + for (size_t i = 0; i < args.size(); i++) { + args[i]->dec(); + } + return NULL; + } + old_vals.push_back(var->val); var->val = args[i++]; } + // Check whether too many arguments were supplied + if (i < args.size()) { + for (size_t i = 0; i < args.size(); i++) { + args[i]->dec(); + } + return NULL; + } + if (dbg_prog) { dbg_prog_indent(cout); cout << "["; @@ -1359,6 +1377,7 @@ Expr *run_code(Expr *_e) { cur = ((CExpr *)prog->kids[1])->kids; i = 0; while((var = (SymExpr *)*cur++)) { + assert(i < args.size()); args[i]->dec(); var->val = old_vals[i++]; } 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)))))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |