search

draperlaboratory / cbat_tools

Program analysis tools developed at Draper on the CBAT project.
MIT License
102 stars 14 forks source link

Error printed when using --show="refuted-goals" in some cases #320

Open gltrost opened 3 years ago

gltrost commented 3 years ago

The message

Uncaught Exception:

  (Failure "Unexpected Expression processing Clause")

appears in the output of wp when running --show="refuted-goals in some examples.

One example is in gltrost/memcpy-example/.../broken_refuted_goals/true.sh. When running ./true.sh, the bottom of the printed information is 

Uncaught Exception:

  (Failure "Unexpected Expression processing Clause")

Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from Bap_wp__Constraint.get_refuted_goals.worker in file "src/constraint.ml", line 473, characters 13-63
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Constraint.get_refuted_goals.worker.(fun) in file "src/constraint.ml", line 479, characters 23-74
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Bap_wp__Output.print_result in file "src/output.ml", line 185, characters 8-74
Called from Wp_analysis.check_pre in file "lib/wp_analysis.ml", line 387, characters 19-115
Called from Wp.callback.(fun) in file "wp.ml", line 351, characters 2-32
Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 25, characters 19-24
Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 23, characters 12-19
Called from Cmdliner.Term.run in file "cmdliner.ml", line 117, characters 32-39
Called from Cmdliner.Term.term_eval in file "cmdliner.ml", line 147, characters 18-36
Called from Cmdliner.Term.eval_choice in file "cmdliner.ml", line 265, characters 22-48
Called from Bap_main.Grammar.eval in file "lib/bap_main/bap_main.ml", line 1054, characters 10-99
Called from Bap_main.init.(fun) in file "lib/bap_main/bap_main.ml", line 1207, characters 15-140
Called from Bap_frontend in file "src/bap_frontend.ml", line 320, characters 8-127