| summaryrefslogtreecommitdiff |
diff options
| author | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-01-31 22:22:04 +0100 |
|---|---|---|
| committer | Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org> | 2017-01-31 22:22:04 +0100 |
| commit | 1dafef5fdf9d98b38cbe717b8a220d721f0ebea8 (patch) | |
| tree | 937e16672b4bdc5d7b75d92a1c60881cd190291a /src/knowledge/knowledge.h | |
| parent | 509ac16d892aeb5091f68620247f6815d2e4b5f5 (diff) | |
Made Frama-C give up.
It validates (*sequence_length == (\old(*sequence_length) + 1))
regardless of the addition of an "*sequence_length -= 1;" in the code.
Diffstat (limited to 'src/knowledge/knowledge.h')
0 files changed, 0 insertions, 0 deletions