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

Optimize Code Mode Patch 1 #84

Open
wants to merge 26 commits into
base: master
Choose a base branch
from
Open

Optimize Code Mode Patch 1 #84

wants to merge 26 commits into from

Conversation

Yiannis128
Copy link
Collaborator

@Yiannis128 Yiannis128 commented Sep 28, 2023

Adds the following features:

  • Support for Arrays and Pointers
  • Removed is_equivalent from AST Declarations as it was unnecessary.
  • OCM command has more verbose error handing. Fixed bug with optimization code
  • Added is_pointer_type() to AST Decl
  • C Types:
    • is_primitive_type now accepts a Declaration instead.
    • Added get_base_type that gets the base type for pointers and lists.
  • Added init depth limit. Pointers get initialized to NULL after limit.

OCM:

  • _generate_primitive_type_variables generates the nondet variables.
  • The OCM function then passes again through the types and
    builds the code.

ESBMC Code Gen Update:

  • Added support for pointers and continuous memory.

* `is_primitive_type` now accepts a Declaration instead.
* Added `get_base_type` that gets the base type for pointers and lists.
* array_expansion
* init_max_depth
* Added pointer and continuous memory support.
* Added init depth limit. Pointers get initialized to NULL after limit.
* Separated logic.
* _generate_primitive_type_variables generates the nondet variables.
* The OCM function then passes again through the types and
builds the code.

ESBMC Code Gen Update:

* Added support for pointers and continuous memory.
* is_pointer_type returns always False
* Added returns_pointer() that returns if a return type is a pointer.
@Yiannis128 Yiannis128 marked this pull request as ready for review October 8, 2023 21:41
@Yiannis128
Copy link
Collaborator Author

Tests need to be written before this is ready.

@Yiannis128 Yiannis128 linked an issue Oct 8, 2023 that may be closed by this pull request
* Added error checking to loadenv
* Added configurable max_attempts
* Removed init_check_health
* Added max attempts from config to FixCodeCommand
* Refactored help output
* Added -e/--env option to specify different env file.
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.

1 participant