Skip to content

Navigation Menu

Appearance settings

View all features
- BY COMPANY SIZE
  Enterprises
  Small and medium teams
  Startups
  Nonprofits
- BY USE CASE
  App Modernization
  DevSecOps
  DevOps
  CI/CD
  View all use cases
- BY INDUSTRY
  Healthcare
  Financial services
  Manufacturing
  Government
  View all industries
View all solutions
- EXPLORE BY TOPIC
  AI
  Software Development
  DevOps
  Security
  View all topics
- EXPLORE BY TYPE
  Customer stories
  Events & webinars
  Ebooks & reports
  Business insights
  GitHub Skills
- SUPPORT & SERVICES
  Documentation
  Customer support
  Community forum
  Trust center
  Partners
- COMMUNITY
  GitHub SponsorsFund open source developers
- PROGRAMS
  Security Lab
  Maintainer Community
  Accelerator
  Archive Program
- REPOSITORIES
  Topics
  Trending
  Collections
- ENTERPRISE SOLUTIONS
  Enterprise platformAI-powered developer platform
- AVAILABLE ADD-ONS
  GitHub Advanced SecurityEnterprise-grade security features
  Copilot for BusinessEnterprise-grade AI features
  Premium SupportEnterprise-grade 24/7 support
Pricing

Search code, repositories, users, issues, pull requests...

Search

Clear

Search syntax tips

Provide feedback

We read every piece of feedback, and take your input very seriously.

Include my email address so I can be contacted

Saved searches

Use saved searches to filter your results more quickly

Name

Query

To see all available qualifiers, see our documentation.

Appearance settings

You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session.

Dismiss alert

model-checking / kani Public

generated from amazon-archives/__template_Apache-2.0

Notifications You must be signed in to change notification settings
Fork 135
Star 2.9k

Code
Issues 455
Pull requests 18
Discussions
Actions
Projects
Security
Insights

Additional navigation options

Code
Issues
Pull requests
Discussions
Actions
Projects
Security
Insights

Make `--gen-c-runnable` produce runnable C code#334

Merged

danielsn merged 82 commits intomodel-checking:main-154-2021-08-17model-checking/kani:main-154-2021-08-17from

vecchiot-aws:gen-c-transformervecchiot-aws/rmc:gen-c-transformerCopy head branch name to clipboard

Aug 20, 2021

Conversation Commits82 (82)Checks Files changed

Merged

Make `--gen-c-runnable` produce runnable C code#334
danielsn merged 82 commits intomodel-checking:main-154-2021-08-17from
vecchiot-aws:gen-c-transformer

Commits

Commits on Aug 20, 2021

Added gen-c transformer.
vecchiot-aws
committed
Add --gen-c-readable flag
vecchiot-aws
committed
Added extra gen-c support.
vecchiot-aws
committed
temporary commit/
vecchiot-aws
committed
Add non_det functions to symbol table.
vecchiot-aws
committed
Fix merge issues and compilation warnings.
vecchiot-aws
committed
Force normalize_identifier to be injective.
vecchiot-aws
committed
Prevent padding from producing unused nondet function calls.
vecchiot-aws
committed
Remove extra files.
vecchiot-aws
committed
Fix missing extern functions (translate to nondet).
vecchiot-aws
committed
Fixed implies operator not existing in C.
vecchiot-aws
committed
Moved removal of macros to after gotoc to avoid missing function error.
vecchiot-aws
committed
Added __CPROVER_atomic_begin/end to gen_c library.
vecchiot-aws
committed
Add default to illegal identifiers.
vecchiot-aws
committed
Add powi and powif to gen_c library.
vecchiot-aws
committed
Add POINTER_OBJECT macro.
vecchiot-aws
committed
Fix illegal default identifier.
vecchiot-aws
committed
Fixed byte_extract_little_endian macro.
vecchiot-aws
committed
Add c-lib to gen-c-runnable and dry_run to gen-c postprocess.
vecchiot-aws
committed
Fix issue with name mapping memory, and don't remove '-' from 'tag-...'
vecchiot-aws
committed
Fix u128 constants not being compilable.
vecchiot-aws
committed
Add --gen-c-runnable back in after rebase.
vecchiot-aws
committed
Fixed issue with tag- appearing in identifiers that weren't structs.
vecchiot-aws
committed
Fix SIMD vector access.
vecchiot-aws
committed
Fix generation of nondet functions with empty return type.
vecchiot-aws
committed
Add gen-c-runnable flag to cargo rmc, and rearrange scripts a bit.
vecchiot-aws
committed
Add purpose flags.
vecchiot-aws
committed
Fix issue with extern functions having no return value.
vecchiot-aws
committed
Fix issue with extern functions returning void.
vecchiot-aws
committed
Fix insert position for include.
vecchiot-aws
committed
Add sputc to list of removals.
vecchiot-aws
committed
Initialize missing extern statics to nondet.
vecchiot-aws
committed
Change transformers to take mutable reference to self.
vecchiot-aws
committed
Remove statics.
vecchiot-aws
committed
Actually remember used names.
vecchiot-aws
committed
Create owned getters for maps.
vecchiot-aws
committed
Restructure gen-c transformer into three parts.
vecchiot-aws
committed
Fixup documentation.
vecchiot-aws
committed
Fix bug with multiple missing parameter identifiers of same type.
vecchiot-aws
committed
Handle return type being empty.
vecchiot-aws
committed
Simplify logic of generating default values in non_det functions.
vecchiot-aws
committed
Revert accidental replacement.
vecchiot-aws
committed
Simplify logic of generating default bodies for extern functions.
vecchiot-aws
committed
Correctly handle when no main function present.
vecchiot-aws
committed
Minor comments and formatting.
vecchiot-aws
committed
Add assert to avoid nondets returning empty.
vecchiot-aws
committed
Fixed bug with generated statics not being global.
vecchiot-aws
committed
Fix issue with parameter names matching local variable names.
vecchiot-aws
committed
Update type_to_string to be injective.
vecchiot-aws
committed
Add docstring.
vecchiot-aws
committed
Fix short-circuiting issue with implies.
vecchiot-aws
committed
Clean up transform_symbol.
vecchiot-aws
committed
Fix transforming bigints to use bit shifting.
vecchiot-aws
committed
Add test for bigints.
vecchiot-aws
committed
Cleanup nondet transformer.
vecchiot-aws
committed
Cleanup name transformer.
vecchiot-aws
committed
Cleanup gen_c_lib
vecchiot-aws
committed
Use binop constructor.
vecchiot-aws
committed
Move transforming 'main' to 'main_' into transform_symbol.
vecchiot-aws
committed
Move type_to_string into typ.rs
vecchiot-aws
committed
Add is_c_integer method to Type.
vecchiot-aws
committed
Clean up bignum_to_expr
vecchiot-aws
committed
Clean up some expr_transformer things.
vecchiot-aws
committed
Add pseudocode for SIMD transformation.
vecchiot-aws
committed
Clarify remembering mapped names is for correctness, not just optimization.
vecchiot-aws
committed
Add clarification for used_names and mapped_names.
vecchiot-aws
committed
Add issue for handling all reserved C names.
vecchiot-aws
committed
Add exapmle for transform_expr_nondet.
vecchiot-aws
committed
Add example for why we need to ignore padding in nondet transformer.
vecchiot-aws
committed
Add note that order matters to passes.rs
vecchiot-aws
committed
Cleanup some stuff in gen_c_lib.c
vecchiot-aws
committed
Switch to not use stcmp.
vecchiot-aws
committed
Change goto-instrument to directly pass in output file.
vecchiot-aws
committed
Added examples to Type.to_identifier for code and variadic_code.
vecchiot-aws
committed
Add documentation to README.
vecchiot-aws
committed
Replace match with if let.
vecchiot-aws
committed
Change .not().not() to cast to bool.
vecchiot-aws
committed
-Create tracking issue for SIMD vector indexing.
vecchiot-aws
committed
Switch overflow to use builtin overflow check functions.
vecchiot-aws
committed
Fix compiler warnings.
vecchiot-aws
committed
Switch imports to be absolute.
vecchiot-aws
committed
Merge branch 'main-154-2021-08-17' into gen-c-transformer
danielsn
authored

Footer

© 2026 GitHub, Inc.

Footer navigation

Terms
Privacy
Security
Status
Community
Docs
Contact

You can’t perform that action at this time.