diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-07-16 15:26:03 +0200 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-07-16 15:26:03 +0200 |
| commit | 67f4ae2b702cc95ed7cef67b726e15abbf18e768 (patch) | |
| tree | 6a28b2b1c7d6feecb12ce810703b356625356231 /kvx/ExpansionOracle.ml | |
| parent | 6121be54b80a55fdadd8b64dfad53357148c9090 (diff) | |
| download | compcert-kvx-67f4ae2b702cc95ed7cef67b726e15abbf18e768.tar.gz compcert-kvx-67f4ae2b702cc95ed7cef67b726e15abbf18e768.zip | |
use a more recognizable option name
Diffstat (limited to 'kvx/ExpansionOracle.ml')
| -rw-r--r--[l---------] | kvx/ExpansionOracle.ml | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/kvx/ExpansionOracle.ml b/kvx/ExpansionOracle.ml index ee2674bf..3b63b80d 120000..100644 --- a/kvx/ExpansionOracle.ml +++ b/kvx/ExpansionOracle.ml @@ -1 +1,17 @@ -../aarch64/ExpansionOracle.ml
\ No newline at end of file +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Léo Gourdin UGA, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +open RTLpathCommon + +let expanse (sb : superblock) code pm = (code, pm) + +let find_last_node_reg c = () |