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

Using package encoding #19

Merged
merged 17 commits into from
Mar 18, 2024
Merged

Using package encoding #19

merged 17 commits into from
Mar 18, 2024

Conversation

julianayang777
Copy link
Contributor

  • Add a flag -p to the command wl test in order to print the results of the execution in stdout.
  • Refactor EvalSymbolic.ml to use the package encoding instead of querying directly with z3 through Translator.ml
    • Refactor heap modules to also use encoding types.

Note that: We did not distinguish Val (Loc n)and Val (Integer n) of type Term.t when evaluating to encoding types, both were evaluated to Val (Int n).

Copy link
Member

@filipeom filipeom left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a few small changes. But it looks great! Can you raise an issue in encoding due to missing simplifications I outline?

dune-project Outdated Show resolved Hide resolved
lib/eval_symbolic.ml Outdated Show resolved Hide resolved
lib/eval_symbolic.ml Outdated Show resolved Hide resolved
lib/eval_symbolic.ml Outdated Show resolved Hide resolved
lib/heap/heap_array_fork.ml Outdated Show resolved Hide resolved
lib/heap/heap_arrayite.ml Outdated Show resolved Hide resolved
lib/heap/heap_tree.ml Outdated Show resolved Hide resolved
test/test_c.t Show resolved Hide resolved
test/test_st.t Show resolved Hide resolved
test/test_st.t Show resolved Hide resolved
@julianayang777
Copy link
Contributor Author

Ok, I will add these issues about simplifications and the one about the concrete execution.

whilloc.opam.template Outdated Show resolved Hide resolved
whilloc.opam Outdated Show resolved Hide resolved
@julianayang777 julianayang777 merged commit 75623a2 into main Mar 18, 2024
2 checks passed
@julianayang777 julianayang777 deleted the encoding branch March 18, 2024 16:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants