'Support of (abstract) map and custom datatype?
In Frama-c w/ WP, I would like to define an abstract model and proves that my C code simulates the abstract model. For example, the abstract model can be an access matrix requiring subjects, objects, and permissions. And subjects can be user processes that have numeric IDs, parent processes, memory contents. In one (not desired) example, the subjects can be defined with datatype Subjects = Subjects(proc_mem:map<int, string>, proc_parent:map<int, int>) in Dafny.
How to define it in Frama-C w/ WP? Any pointers would be appreciated. And what would be the suggested procedure to perform this task under Frama-C w/ WP?
My frama-c setup: Frama-c 24.0, Ubuntu 20.04.4 x64
Read some of the document: frama-c-acsl-implementation.pdf, still got no clue.
Sources
This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.
Source: Stack Overflow
| Solution | Source |
|---|