6 of 6 standards met
Adds support for boxes for pirmitive types. Adds a new builtin function boxnew with a model that allocates data on the heap and returns a pointer. Added support for rust builtins by adding a default return type and default_type for rust Since rust type system is quite elaborate with heap allocated types support for adding charon arguments is added to remove some of the boiler plate with arguments like --hide-marker-trait and --hide-allocator. Additionaly we give a warning if we encounter type definitions or functions that cannot be translated instead of dying so that it is still possible to analyze the functions we do support.
This PR introduces initial translation of a small subset of rust programs. We moved from creating our own library for translating rust programs, to use the charon library. This libraries can digest rust programs and crates with their dependencies and turning them into a uniform and usable shape stored in a json file which can be read by charons OCAMl bindings. The main changes / additions in this pr are as follows: : Changed from loading in textual files by our external library to read and translate the json file produced by charon. : The main addition where the actual translation from rust to textual happends. : The test folder, the folder is structed as followings: : This folder contains test files where each test has three files: : The rust program : The intermediate representation of the rust program in charons json format : The intermediate representation of the rust program in human readable format : Contain the expected output of the tests The next steps are 1. To implement the following rust types: Non-Empty Tuples: Empty tuples are treated as the unit type and are already handled. The next step is to implement non-empty tuples. Arrays: Do not hard-code the array type as int; instead, use the type information from builtin_ty provided by Charon. ADTs: ADTs other than tuples and arrays must also be implemented to support structs. Aggregates: Empty aggregates are already handled, but non-empty aggregates must be supported as well. String and Box:** Heap-allocated types such as strings and boxes must be supported. 2. Model some of rusts standard library in textual 3. Expand tests, and add end to end tests in For more details and outputs from sample programs, the report: Infer_Rust_Frontend_Implementation___Testing.pdf For a overview of the translation rules from rusts intermediate representation you can refer to the following report: translation rules.pdf Would love to hear your feedback!
Repository: facebook/infer. Description: A static analyzer for Java, C, C++, and Objective-C Stars: 15527, Forks: 2071. Primary language: OCaml. Languages: OCaml (72.4%), Java (6.9%), C++ (6.7%), Objective-C (3.2%), Makefile (2.6%). License: MIT. Homepage: http://fbinfer.com/ Topics: c, code-quality, cpp, java, objective-c, static-analysis, static-code-analysis. Latest release: v1.2.0 (1y ago). Open PRs: 9, open issues: 401. Last activity: 1d ago. Community health: 87%. Top contributors: jvillard, jberdine, dulmarod, skcho, ngorogiannis, sblackshear, davidpichardie, jeremydubreil, ezgicicek, mbouaziz and others.
OCaml
Last 12 weeks ยท 211 commits
Hello everybody, I noticed in the source code most test Makefiles use --no-pulse-force-continue for the Pulse checker. I found comments in the source code noting that pulse-force-continue "may introduce false positives" (PulseCallOperations.ml:987-989). For a large production codebase where reducing false positives is a priority (accepting that some true positives may be missed), should I set pulse-force-continue and pulse-havoc-arguments** to false? What configuration do you recommend for production use of the Pulse checker? Thank you again for your time and guidance.