Comments (2)
My solution to this issue:
Functions, Modules, Structs can have an attribute to disable the compilers dead_code lint.
If piece of code was marked by #[allow(dead_code)] I suggest to add a comment on top of this piece of code, stating that this function (Struct, module) was ignored by the compiler and should not be verified.
so Coq
code should look like this:
a7328a3
from coq-of-rust.
Done
from coq-of-rust.
Related Issues (20)
- Translate the example inline_assembly_memory_address_operands.v
- Translate the example inline_assembly_options.v
- Translate the example inline_assembly_register_template_modifiers.v
- Translate the example inline_assembly_scratch_register.v
- Translate the example inline_assembly_symbol_operands_and_abi_clobbers.v
- Translate the example inline_assembly.v
- Translate the example raw_pointers.v
- Translate the example declare_first.v
- Translate the example arc.v
- Translate the example file_io_read_lines_efficient_method.v
- Translate the example calling_unsafe_functions.v
- Handle &dyn at top-level of functions
- Verify swap example
- Make functions of a single parameter
- State.Trait parameter support for parameters and global instances
- Getters for type aliases
- Remove core.marker.Sized.Trait
- Add ERC-1155, multisigs, and flipper
- Add copy for function calls and lets
- Have distinct integer types
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from coq-of-rust.