From 25b266d26f16297004a57110d95975ee16145d20 Mon Sep 17 00:00:00 2001 From: Lorenzo Manacorda Date: Wed, 29 Jan 2020 12:05:39 +0100 Subject: [PATCH 1/3] rename rules.k.tmp to rules.k --- lib/build.js | 2 +- resources/{rules.k.tmp => rules.k} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename resources/{rules.k.tmp => rules.k} (100%) diff --git a/lib/build.js b/lib/build.js index 5f64f63a..a05d0f0d 100644 --- a/lib/build.js +++ b/lib/build.js @@ -175,7 +175,7 @@ endmodule .join("\n") const rules_k = rules_template([ - fs.readFileSync(path.join(__dirname, "../resources/rules.k.tmp")).toString(), + fs.readFileSync(path.join(__dirname, "../resources/rules.k")).toString(), rules ]) const rules_path = path.join(KLAB_OUT, "rules.k"); diff --git a/resources/rules.k.tmp b/resources/rules.k similarity index 100% rename from resources/rules.k.tmp rename to resources/rules.k From b534129cb6e80bccb6bae98bc34cce1a599bfd13 Mon Sep 17 00:00:00 2001 From: Lorenzo Manacorda Date: Wed, 29 Jan 2020 12:05:51 +0100 Subject: [PATCH 2/3] README: document rules.k --- README.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/README.md b/README.md index 1aa52290..cb803abd 100644 --- a/README.md +++ b/README.md @@ -100,6 +100,12 @@ Once the proof is complete, we can explore the generated symbolic execution trac klab debug ``` +### Embedded rules + +klab comes with a set of pre-defined K rewrite rules, additional to the ones +defined in [evm-semantics](https://github.com/kframework/evm-semantics). They +are located in `resources/rules.k`. + ### Key Bindings Toggle different views by pressing any of the following keys: From 48ccbf8f0c5b809098873f506ead9675f162bf62 Mon Sep 17 00:00:00 2001 From: Lorenzo Manacorda Date: Fri, 31 Jan 2020 16:53:34 +0100 Subject: [PATCH 3/3] rename to rules.k.tmpl Because it's not a valid K file, since it lacks module wrapper and imports. --- README.md | 2 +- lib/build.js | 2 +- resources/{rules.k => rules.k.tmpl} | 0 3 files changed, 2 insertions(+), 2 deletions(-) rename resources/{rules.k => rules.k.tmpl} (100%) diff --git a/README.md b/README.md index cb803abd..7bffb426 100644 --- a/README.md +++ b/README.md @@ -104,7 +104,7 @@ klab debug klab comes with a set of pre-defined K rewrite rules, additional to the ones defined in [evm-semantics](https://github.com/kframework/evm-semantics). They -are located in `resources/rules.k`. +are located in `resources/rules.k.tmpl`. ### Key Bindings diff --git a/lib/build.js b/lib/build.js index a05d0f0d..a1fcc7be 100644 --- a/lib/build.js +++ b/lib/build.js @@ -175,7 +175,7 @@ endmodule .join("\n") const rules_k = rules_template([ - fs.readFileSync(path.join(__dirname, "../resources/rules.k")).toString(), + fs.readFileSync(path.join(__dirname, "../resources/rules.k.tmpl")).toString(), rules ]) const rules_path = path.join(KLAB_OUT, "rules.k"); diff --git a/resources/rules.k b/resources/rules.k.tmpl similarity index 100% rename from resources/rules.k rename to resources/rules.k.tmpl