diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-12 19:09:42 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-12 19:09:42 +0200 |
| commit | 3b0bbd7a60771265ff81cc98310d413130ae4d79 (patch) | |
| tree | 7a77101325f2eb2c5a97488df0c44da218e40ddf /backend/Asmexpandaux.ml | |
| parent | 9873f9ee01c6ccca88fd461d318e107ff303fe88 (diff) | |
| download | compcert-kvx-3b0bbd7a60771265ff81cc98310d413130ae4d79.tar.gz compcert-kvx-3b0bbd7a60771265ff81cc98310d413130ae4d79.zip | |
Changed definition of implem for debug information.
Instead of making each filed mutuable we use a reference to a record
of type implem. Now only the default implementation and the default
debug information need to be upated to add a new function.
Bug 17392.
Diffstat (limited to 'backend/Asmexpandaux.ml')
| -rw-r--r-- | backend/Asmexpandaux.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml index 59d8d8db..3b77f135 100644 --- a/backend/Asmexpandaux.ml +++ b/backend/Asmexpandaux.ml @@ -94,8 +94,7 @@ let expand_debug id sp preg simple l = lbl | Some lbl -> lbl in let rec aux lbl scopes = function - | [] -> let lbl = get_lbl lbl in - Debug.function_end id lbl + | [] -> () | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest -> let kind = (P.to_int kind) in begin |