Commit 386c29e6 authored by Maxime Perrotin's avatar Maxime Perrotin

Update string templates

parent 458c21bb
/*
* Copyright (c) 2016 European Space Agency
*
* This file is a custom backend to be used with the ASN1SCC tool.
* It generates an Ada package with iterators that compute all possible values
* of all ASN.1 types.
*
* Licensed under the terms of GNU General Public Licence as published by
* the Free Software Foundation.
*
*/
group ada_iterators;
//delimiters "$", "$"
/* Header of the file */
RootXml(arrsFiles) ::= <<
-- This file was generated automatically by TASTE: DO NOT EDIT
-- Dummy package that is used to "with" the ASN.1 modules
$arrsFiles;separator="\n"$
package ASN1_Ada_Iterators is
end;
>>
/* sFileName is a string with the current file name */
FileXml(sFileName, arrsModules) ::= <<
-- ASN.1 File $sFileName$
$arrsModules;separator="\n"$
>>
ModuleXml(sName, sCName, arrsImportedModules, arrsExpTypes, arrsExpVars, arrsTases, arrsVases) ::=<<
with $sCName$;
use $sCName$;
pragma Unreferenced($sCName$);
>>
ImportedMod(sName, sCName, arrsTypes, arrsVars) ::= ""
TasXml(sName, nLine, nPos, sType, sCName, sAssigOp, sContract) ::= ""
VasXml(sName, nLine, nPos, sType, sValue, sCName) ::= ""
TypeGeneric(nLine, nPos, sAsnFile, sSubType) ::= ""
MinMaxType(sName, sMin, sMax, bFixedSize, bIsUnsigned, bIsRealType) ::= ""
MinMaxType2(sName, sMin, sMax, bFixedSize) ::= ""
BooleanType () ::= ""
NullType () ::= ""
IntegerType () ::= ""
RealType () ::= ""
BitStringType () ::= ""
OctetStringType () ::= ""
IA5StringType () ::= ""
NumericStringType () ::= ""
AssigOpNormalType () ::= ""
AssigOpSpecialType () ::= ""
EnumItem (sName, sCName, nVal, nLine, nPos, sCID) ::= ""
EnumType(arrsItems) ::= ""
ChoiceChild(sName, sCName, nLine, nPos, sChildContent, sNamePresent ) ::= ""
ChoiceType(arrsChildren) ::= ""
SequenceChild(sName, sCName, bOptional, sDefVal, nLine, nPos, sChildContent ) ::= ""
SequenceType(arrsChildren) ::= ""
SequenceOfType(sMin, sMax, sChild, bFixedSize) ::= ""
RefTypeMinMax(sMin, sMax, sName, sModName, sCName, sCModName, bFixedSize) ::= ""
RefType(sName, sModName, sCName, sCModName) ::= ""
Contract(sTypePattern, sExpr) ::= ""
TypePatternCommonTypes() ::= ""
TypePatternSequence(sName, sCName, arrsChildren) ::= ""
SequencePatternChild(sName, sCName) ::= ""
ContractExprMinMax(sPattern, sMin, sMax, bFixedSize) ::= ""
ContractExprSize(sPattern, sMin, sMax, bFixedSize) ::= ""
ContractExprSequence(arrsChildren) ::= ""
Print_IntegerValue(nVal) ::= ""
Print_RealValue(dVal) ::= ""
Print_StringValue(v) ::= ""
Print_TrueValue() ::= ""
Print_FalseValue() ::= ""
Print_BitStringValue(v) ::= ""
Print_OctetStringValue(arruOctets) ::= ""
Print_RefValue(sName) ::= ""
Print_SeqOfValue(arrsValues) ::= ""
Print_SeqValue_Child(sName, sChildValue) ::= ""
Print_SeqValue(arrsValues) ::= ""
Print_ChValue(sAltName,sAltValue) ::= ""
Print_NullValue() ::= ""
/*
* Copyright (c) 2016 European Space Agency
*
* This file is a custom backend to be used with the ASN1SCC tool.
* It generates an Ada package with iterators that compute all possible values
* of all ASN.1 types.
*
* Licensed under the terms of GNU General Public Licence as published by
* the Free Software Foundation.
*
*/
group ada_iterators;
//delimiters "$", "$"
/* Header of the file */
RootXml(arrsFiles) ::= <<
-- This file was generated automatically by TASTE: DO NOT EDIT
-- Dummy package that is used to "with" the ASN.1 modules
$arrsFiles;separator="\n"$
package ASN1_Ada_Iterators is
end;
>>
/* sFileName is a string with the current file name */
FileXml(sFileName, arrsModules) ::= <<
-- ASN.1 File $sFileName$
$arrsModules;separator="\n"$
>>
ModuleXml(sName, sCName, arrsImportedModules, arrsExpTypes, arrsExpVars, arrsTases, arrsVases) ::=<<
with $sCName$;
use $sCName$;
pragma Unreferenced($sCName$);
>>
ImportedMod(sName, sCName, arrsTypes, arrsVars) ::= ""
TasXml(sName, nLine, nPos, sType, sCName, sAssigOp, sContract, bAddedType) ::= ""
VasXml(sName, nLine, nPos, sType, sValue, sCName) ::= ""
TypeGeneric(nLine, nPos, sAsnFile, sSubType, bHasAcnEncDecFunction) ::= ""
MinMaxType(sName, sMin, sMax, bFixedSize, bIsUnsigned, bIsRealType) ::= ""
MinMaxType2(sName, sMin, sMax, bFixedSize) ::= ""
BooleanType () ::= ""
NullType () ::= ""
IntegerType () ::= ""
RealType () ::= ""
BitStringType () ::= ""
OctetStringType () ::= ""
IA5StringType () ::= ""
NumericStringType () ::= ""
AssigOpNormalType () ::= ""
AssigOpSpecialType () ::= ""
EnumItem (sName, sCName, nVal, nLine, nPos, sCID) ::= ""
EnumType(arrsItems) ::= ""
ChoiceChild(sName, sCName, nLine, nPos, sChildContent, sNamePresent ) ::= ""
ChoiceType(arrsChildren) ::= ""
SequenceChild(sName, sCName, bOptional, sDefVal, nLine, nPos, sChildContent ) ::= ""
SequenceType(arrsChildren) ::= ""
SequenceOfType(sMin, sMax, sChild, bFixedSize) ::= ""
RefTypeMinMax(sMin, sMax, sName, sModName, sCName, sCModName, bFixedSize, soResolvedType) ::= ""
RefType(sName, sModName, sCName, sCModName) ::= ""
Contract(sTypePattern, sExpr) ::= ""
TypePatternCommonTypes() ::= ""
TypePatternSequence(sName, sCName, arrsChildren) ::= ""
SequencePatternChild(sName, sCName) ::= ""
ContractExprMinMax(sPattern, sMin, sMax, bFixedSize) ::= ""
ContractExprSize(sPattern, sMin, sMax, bFixedSize) ::= ""
ContractExprSequence(arrsChildren) ::= ""
Print_IntegerValue(nVal) ::= ""
Print_RealValue(dVal) ::= ""
Print_StringValue(v) ::= ""
Print_TrueValue() ::= ""
Print_FalseValue() ::= ""
Print_BitStringValue(v) ::= ""
Print_OctetStringValue(arruOctets) ::= ""
Print_RefValue(sName) ::= ""
Print_SeqOfValue(arrsValues) ::= ""
Print_SeqValue_Child(sName, sChildValue) ::= ""
Print_SeqValue(arrsValues) ::= ""
Print_ChValue(sAltName,sAltValue) ::= ""
Print_NullValue() ::= ""
......@@ -39,6 +39,7 @@ def event (interface: str, sort: str, param: bool) -> str:
res += f'''
null;
'''
return res
def print_event (interface: str, sort: str, param : bool) -> str:
if param:
......@@ -178,7 +179,7 @@ begin
Check_And_Report(Start_Hash);
ES.Queue.append(Start_Hash);
Visited.Include(Start_Hash);
while ES.Queue.Length > 0 and Properties.Length \<= 10 loop
while ES.Queue.Length > 0 and Properties.Length <= 10 loop
Process_Ctxt := Grafset.Element(Key => ES.Queue.Last_Element).Context;
Exhaustive_Simulator;
ES.Queue.Delete_Last;
......@@ -249,7 +250,7 @@ def generate(ast, stop_conditions):
print_events=print_events,
check_properties=check_ppties,
exhaust_procedures=exhaust_procedures,
exhausts=exhauts)
exhausts=exhausts)
with open('model_checker.adb', 'wb') as ada_file:
ada_file.write(complete.encode('latin1'))
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment