Merge pull request #111 from casm-lang/release/0.6.0

Release/0.6.0

doc/language/grammar/FunctionDefinition.org

@@ -8,3 +8,9 @@ Furthermore, due to the fact that ASM functions are by default =undef= (undefine
 #+html: <callout type="info" icon="true">
 This definition is introduced in version =0.1.0=. 
 #+html: </callout>
+
+In order to evaluate a CASM function as symbolic in the symbolic/concolic execution and include it in the TPTP trace, the function has to set the attribute =symbolic=
+
+#+html: <callout type="info" icon="true">
+The attribute =symbolic= is introduced in version =0.6.0=. 
+#+html: </callout>

doc/release/0.6.0.org

@@ -0,0 +1,63 @@
+# 
+#   Copyright (C) 2014-2021 CASM Organization <https://casm-lang.org>
+#   All rights reserved.
+# 
+#   Developed by: Philipp Paulweber
+#                 Emmanuel Pescosta
+#                 <https://github.com/casm-lang/casm>
+# 
+#   This file is part of casm.
+# 
+#   casm is free software: you can redistribute it and/or modify
+#   it under the terms of the GNU General Public License as published by
+#   the Free Software Foundation, either version 3 of the License, or
+#   (at your option) any later version.
+# 
+#   casm is distributed in the hope that it will be useful,
+#   but WITHOUT ANY WARRANTY; without even the implied warranty of
+#   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+#   GNU General Public License for more details.
+# 
+#   You should have received a copy of the GNU General Public License
+#   along with casm. If not, see <http://www.gnu.org/licenses/>.
+# 
+#
+
+#+options: toc:nil
+#+html: {{tag>release}}
+
+*** 0.6.0
+
+#+html: <callout title="Release ''faidros''">
+[[https://github.com/casm-lang/casm/releases/tag/0.6.0][{{fa>github?lg}}]] June 6, 2021
+
+The release identifier [[http://www.behindthename.com/name/phaedrus][faidros]]
+is derived from the Greek name Φαιδρος (Phaidros) and means "bright".
+#+html: </callout>
+
+#+html: <grid>
+#+html: <col lg="6" md="12">
+#+html: <TEXT align="justify">
+This is the sixth official release of the CASM project.
+We are happy to present our new symbolic/concolic execution functionality.
+Basis for the CASM symbolic execution is a complete from scratch implemented C++ library called =libtptp= which provides a TPTP parser, code emitter, and evaluation transformation towards Z3.
+By annotating CASM functions with the attribute =symbolic= allows the CASM symbolic execution to derive first order formula based TPTP traces of the desired annotated functions.
+Furthermore, we support the complete building by (open-)source of the three main applications =casmd=, =casmf=, and =casmi= and the corresponding libraries like =libcasm-fe= or =libcasm-ir=.
+
+#+html: </TEXT>
+#+html: </col>
+#+html: <col lg="6" md="12">
+
+| {{fa>file-alt?lg}}     | *Language*    | We enabled the =symbolic= attribute for [[./../syntax#FunctionDefinition][function definition]] language elements to annotate functions that shall be symbolically evaluated during the concolic execution. |
+|                        |               |                                                                                                                                                                         |
+| {{fa>terminal?lg}}     | *Application* | Provided a new command line option (=-s=) to the CASM interpreter application =casmi= to evaluate CASM specifications with the new concolic execution.                  |
+|                        |               |                                                                                                                                                                         |
+| {{fa>terminal?lg}}     | *Application* | Enabled the concolic execution support in the CASM language server daemon application =casmd= for LSP-based editor integration to invoke concolic executions.           |
+|                        |               |                                                                                                                                                                         |
+| {{fa>puzzle-piece?lg}} | *Plug-in*     | Integrated a new LSP command in the =monaco= editor extension to invoke CASM concolic executions and render the generated TPTP trace.                                   |
+|                        |               |                                                                                                                                                                         |
+| {{fa>microchip?lg}}    | *Environment* | Full open-source based compilations of libraries and applications.                                                                                                      |
+|                        |               |                                                                                                                                                                         |
+
+#+html: </col>
+#+html: </grid>