Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
gltrost opened this issue May 7, 2021 · 0 comments
Open

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

gltrost opened this issue May 7, 2021 · 0 comments
Labels
bug Something isn't working

Comments

@gltrost
Copy link
Contributor

gltrost commented May 7, 2021

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
@gltrost gltrost added the bug Something isn't working label May 7, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant