Follow
The new bane of my existence, uncommented Coq code.
Axiom ef_deterministic_fun:
forall ef,
ef_deterministic ef = true ->
forall ge args m t1 t2 vres1 vres2 m1 m2,
Events.external_call ef ge args m t1 vres1 m1 ->
Events.external_call ef ge args m t2 vres2 m2 ->
(vres1,t1,m1) = (vres2,t2,m2).
Gee thanks... Not only is one of the most conceptually complex languages mankind has come up with, it has that single letter fetishism that mathematicians tend to have.
@jmw150
From here
https://github.com/PrincetonUniversity/VST
What I can guess is that:
ef_deterministic_fun is a rule for external functions that are deterministic to tell if they are equivalent. This is for software that is used to formally prove that C programs are doing what we think they are.
Not sure why 'fun' is added at the end. It is common shorthand for function. But anyway, next bit:
This is the function ef, if this boolean function comes back true, these other conditions are true.
Definition ef_deterministic (ef: external_function) : bool :=
match ef with
| EF_external name sg => false
| EF_builtin name sg => true
| EF_runtime name sg => false
| EF_vload chunk => false
| EF_vstore chunk => false
| EF_malloc => true
| EF_free => true
| EF_memcpy sz al => true
| EF_annot kind text targs => true
| EF_annot_val kind Text rg => true
| EF_inline_asm text sg clob => false
| EF_debug kind text targs => true
end.
- What is 'ge'? Global environment?
- args are probably arguments
- m, m1, m2 are a mystery, I am guessing either a stack or a heap
- t1, t2 maybe stack or heap
- vres maybe a command of some sort
Thankfully Inria people are better at things. Probably because they are selling the C compiler, and can have professionals instead of students.
ef external function
ge global environment?
args to the function
m for memory state before call
t1?
vres is result value
m1 for memory state after call