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.

Sign up for GitHub

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

Jump to bottom

SMV: expression typechecker now post-traversal #1040

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

SMV: expression typechecker now post-traversal #1040

wants to merge 2 commits into from

Conversation

kroening
Copy link
Member

This hoists the recursive call to typecheck the expression operands out of the case split, i.e., operands are always typechecked first.

@kroening
SMV: expression typechecker now post-traversal
dc998f6 
This hoists the recursive call to typecheck the expression operands out of
the case split, i.e., operands are always typechecked first.
@kroening kroening added the SMV label Mar 28, 2025
@kroening kroening mentioned this pull request Mar 28, 2025
Open
@kroening kroening marked this pull request as ready for review March 28, 2025 19:29
@mgudemann
Copy link
Contributor

For me, this change leads to the same problem

~/s/g/H/hw-cbmc (smv-tc-expr-traversal|✚1) $ ./ebmc  AIG_SMV/dintel048.aig/intel048.aig.smv
Parsing AIG_SMV/dintel048.aig/intel048.aig.smv
Converting
Type-checking smv::main
fish: Job 1, './ebmc  AIG_SMV/dintel048.aig/i…' terminated by signal SIGSEGV (Address boundary error)

adding a counter shows a recursion depth is over 3271 for the above.
I think this really only concerns models converted to SMV from AIG.

@kroening
SMV: stack-based expression type checking
17ede1a 
To address #17, this replaces the recusion in the SMV expression type
checker by exprt::visit_post.

Closes #17
@mgudemann
Copy link
Contributor

still this behavior

  main                           0ec55ad4 [behind 8] Merge pull request #1036 from mgudemann/fix/unused-vars-in-assert
  master                         7995ac3a Merge pull request #63 from diffblue/update-test-pl
* smv-tc-expr-traversal          17ede1a9 SMV: stack-based expression type checking
~/s/g/H/hw-cbmc (smv-tc-expr-traversal|✚1) $ ./ebmc --k-induction AIG_SMV/dintel048.aig/intel048.aig.smv 
Parsing AIG_SMV/dintel048.aig/intel048.aig.smv
Converting
Type-checking smv::main
fish: Job 1, './ebmc --k-induction AIG_SMV/di…' terminated by signal SIGSEGV (Address boundary error)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
SMV
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@kroening @mgudemann