Comments (2)
davidcok
commented on June 12, 2024
Since ghost code is already in an annotation comment, does the specification for the ghost code need to be in an embedded comment? Or would omitting such delimiters make problems for the parser?
from acsl.
vprevosto
commented on June 12, 2024
Omitting the delimiters would indeed complicate things for the parser, as ACSL and C (ghost or not) syntaxes are quite different. Having delimiters makes it easy to know when to switch between the two.
In addition, the development version of Frama-C recently gained support for /@ @/ in ghost code, making the issue rather moot.
from acsl.
Related Issues (20)
- axiomatic blocks as namepaces HOT 3
- Nested axiomatic blocks HOT 3
- Floating point comparison HOT 6
- Release of ACSL 1.12 HOT 3
- Taking the address of a formal in a function contract HOT 7
- Paragraph in the right margin HOT 2
- ACSL++ virtual logic functions
- scope of ghost local variables
- Structures, Unions and Arrays in logic HOT 2
- Considering a valid pointer and an invalid pointer, should they be `\separated()`? HOT 4
- Exact program state of Pre and Post states HOT 16
- Clarification on meaning of \valid HOT 10
- type-expr is defined twice HOT 2
- Notation for non-finite floating-point values HOT 2
- Clarification on order of arguments for termination measure HOT 1
- Support of 'L' suffix for floating-point literals of type long double, and `D` for literals of type double HOT 2
- Links between `\initialized{L}(p)` and `\valid_read{L}(p)`. HOT 2
- Proposal for meaning of `\valid`, `\valid_read` w.r.t. `\initialized` HOT 8
- Clarification about label Pre
- Unbound logic variable warning when using .. to specify array length, i.e. \valid(buckets+(0..{x})), when {x} is a global variable HOT 2
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 acsl.