Opened 16 years ago
Closed 16 years ago
#268 closed defect (fixed)
no extra locations for collective assertions...
| Reported by: | Stephen Siegel | Owned by: | zirkel |
|---|---|---|---|
| Priority: | major | Milestone: | 1.1 |
| Component: | front | Version: | 1.1 |
| Keywords: | pragma collective assertion invariant joint | Cc: |
Description
A {joint,collective,} {assertion,invariant} specified as a pragma should never add a location to a model. It should only set values in a particular location. The philosophy is that you don't want "Heisenbugs" arising from modifying the model you are trying to analyze.
If the pragma is inserted in a "bad" place---a place that does not really have a location associated to it --- a syntax error should be thrown saying something to the effect "No location at this position". The bad places are ends of blocks in "if" statements, loops, etc.
If a user wants to add a pragma at such a point, he can introduce a location by just adding a ";" (empty statement) after the pragma.
Note:
See TracTickets
for help on using tickets.
Syntax exceptions should now be thrown for bad places. Note that a for loop is syntactic sugar for an init statement and a while loop with the update statement added to the end. In a for with a non-empty update, the assertion will be associated with the update location. For a void function with no explicit return, the assertion will be associated with the implicit return.