diff options
| author | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-04 03:04:21 +0100 |
|---|---|---|
| committer | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2015-11-04 03:04:21 +0100 |
| commit | 5664fddcab15ef4482d583673c75e07bd1e96d0a (patch) | |
| tree | 878b22860e69405ba5cf6fd2798731dac8ce660c /backend/LTL.v | |
| parent | b960c83725d7e185ac5c6e3c0d6043c7dcd2f556 (diff) | |
| parent | fe73ed58ef80da7c53c124302a608948fb190229 (diff) | |
| download | compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.tar.gz compcert-5664fddcab15ef4482d583673c75e07bd1e96d0a.zip | |
Merge remote-tracking branch 'origin/master' into parser_fix
Diffstat (limited to 'backend/LTL.v')
| -rw-r--r-- | backend/LTL.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/LTL.v b/backend/LTL.v index 67fb0197..48c5c850 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -77,8 +77,8 @@ Definition genv := Genv.t fundef unit. Definition locset := Locmap.t. (** Calling conventions are reflected at the level of location sets - (environments mapping locations to values) by the following two - functions. + (environments mapping locations to values) by the following two + functions. [call_regs caller] returns the location set at function entry, as a function of the location set [caller] of the calling function. @@ -87,7 +87,7 @@ Definition locset := Locmap.t. values as the corresponding outgoing stack slots (used for argument passing) in the caller. - Local and outgoing stack slots are initialized to undefined values. -*) +*) Definition call_regs (caller: locset) : locset := fun (l: loc) => |