blob: f3f6198b0ca06b005659fd660e293af6040e4929 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
+++
title = "Issue with Main"
date = "2021-02-17"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a1"]
forwardlinks = []
zettelid = "3a1a"
+++
the `main` function in CompCert can not arguments any arguments. In the
rules for programs going wrong initially, if the initial state cannot be
constructed, then the program will go wrong, which means that none of
the correctness proofs can be said to hold.
``` coq
| program_goes_initially_wrong:
(forall s, ~initial_state L s) ->
program_behaves (Goes_wrong E0).
```
The initial state can also only be constructed if the signature of the
first function that is called is of `signature_main`, which can only be
of the function type without arguments.
``` coq
Inductive initial_state (p: program): state -> Prop :=
| initial_state_intro: forall b f m0,
...
funsig f = signature_main ->
initial_state p (Callstate nil f nil m0).
```
|
