Last active
August 29, 2015 14:04
-
-
Save ytomino/ed2ada3abf4e6d8c09ee to your computer and use it in GitHub Desktop.
SPARKで遊んでみた
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| pragma Annotate (GNATprove, External_Axiomatization); | |
| package test1 | |
| with Pure, SPARK_Mode | |
| is | |
| function fact (x : Integer) return Integer is | |
| (if x > 0 then | |
| x * fact (x - 1) -- overflow check might fail | |
| else | |
| 1); | |
| end test1; | |
| -- $ gnatprove -Ptests --mode=all test1.ads | |
| -- Phase 1 of 3: frame condition computation ... | |
| -- Phase 2 of 3: analysis and translation to intermediate language ... | |
| -- Phase 3 of 3: generation and proof of VCs ... | |
| -- analyzing test1, 0 checks | |
| -- analyzing test1.fact, 2 checks | |
| -- test1.ads:8:12: warning: overflow check might fail | |
| -- gprbuild: *** compilation phase failed | |
| -- gnatprove: error during generation and proof of VCs, aborting. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* Module for axiomatizing type "short_short_integer", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__short_short_integer | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type short_short_integer "bounded_type" | |
| function first | |
| :int = | |
| ( -128 ) | |
| function last | |
| :int = | |
| 127 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = short_short_integer, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "short_integer", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__short_integer | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type short_integer "bounded_type" | |
| function first | |
| :int = | |
| ( -32768 ) | |
| function last | |
| :int = | |
| 32767 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = short_integer, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "integer", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__integer | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type integer "bounded_type" | |
| function first | |
| :int = | |
| ( -2147483648 ) | |
| function last | |
| :int = | |
| 2147483647 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = integer, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "long_integer", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__long_integer | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type long_integer "bounded_type" | |
| function first | |
| :int = | |
| ( -9223372036854775808 ) | |
| function last | |
| :int = | |
| 9223372036854775807 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = long_integer, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "long_long_integer", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__long_long_integer | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type long_long_integer "bounded_type" | |
| function first | |
| :int = | |
| ( -9223372036854775808 ) | |
| function last | |
| :int = | |
| 9223372036854775807 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = long_long_integer, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "natural", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__natural | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type natural "bounded_type" | |
| function first | |
| :int = | |
| 0 | |
| function last | |
| :int = | |
| 2147483647 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = natural, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "positive", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__positive | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type positive "bounded_type" | |
| function first | |
| :int = | |
| 1 | |
| function last | |
| :int = | |
| 2147483647 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = positive, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "short_float", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__short_float | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Floating | |
| use import "real".RealInfix | |
| type short_float "bounded_type" | |
| function first | |
| :real = | |
| (-.340282346638528859811704183484516925440.0) | |
| function last | |
| :real = | |
| (340282346638528859811704183484516925440.0) | |
| predicate in_range | |
| (x : real) = | |
| ( ( first <=. x ) /\ ( x <=. last ) ) | |
| clone export "ada__model".Static_Floating_Point with | |
| type t = short_float, | |
| function round_real_tmp = Floating.round_single, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "float", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__float | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Floating | |
| use import "real".RealInfix | |
| type float "bounded_type" | |
| function first | |
| :real = | |
| (-.340282346638528859811704183484516925440.0) | |
| function last | |
| :real = | |
| (340282346638528859811704183484516925440.0) | |
| predicate in_range | |
| (x : real) = | |
| ( ( first <=. x ) /\ ( x <=. last ) ) | |
| clone export "ada__model".Static_Floating_Point with | |
| type t = float, | |
| function round_real_tmp = Floating.round_single, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "long_float", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__long_float | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Floating | |
| use import "real".RealInfix | |
| type long_float "bounded_type" | |
| function first | |
| :real = | |
| (-.179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0) | |
| function last | |
| :real = | |
| (179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0) | |
| predicate in_range | |
| (x : real) = | |
| ( ( first <=. x ) /\ ( x <=. last ) ) | |
| clone export "ada__model".Static_Floating_Point with | |
| type t = long_float, | |
| function round_real_tmp = Floating.round_double, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "long_long_float", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__long_long_float | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Floating | |
| use import "real".RealInfix | |
| type long_long_float "bounded_type" | |
| function first | |
| :real = | |
| (-.1189731495357231765021263853030970205169063322294624200440323733891737005522970722616410290336528882853545697807495577314427443153670288434198125573853743678673593200706973263201915918282961524365529510646791086614311790632169778838896134786560600399148753433211454911160088679845154866512852340149773037600009125479393966223151383622417838542743917838138717805889487540575168226347659235576974805113725649020884855222494791399377585026011773549180099796226026859508558883608159846900235645132346594476384939859276456284579661772930407806609229102715046085388087959327781622986827547830768080040150694942303411728957777100335714010559775242124057347007386251660110828379119623008469277200965153500208474470792443848545912886723000619085126472111951361467527633519562927597957250278002980795904193139603021470997035276467445530922022679656280991498232083329641241038509239184734786121921697210543484287048353408113042573002216421348917347174234800714880751002064390517234247656004721768096486107994943415703476320643558624207443504424380566136017608837478165389027809576975977286860071487028287955567141404632615832623602762896316173978484254486860609948270867968048078702511858930838546584223040908805996294594586201903766048446790926002225410530775901065760671347200125846406957030257138960983757998926954553052368560758683179223113639519468850880771872104705203957587480013143131444254943919940175753169339392366881856189129931729104252921236835159922322050998001677102784035360140829296398115122877768135706045789343535451696539561254048846447169786893211671087229088082778350518228857646062218739702851655083720992349483334435228984751232753726636066213902281264706234075352071724058665079518217303463782631353393706774901950197841690441824738063162828586857741432581165364040218402724913393320949219498422442730427019873044536620350262386957804682003601447291997123095530057206141866974852846856186514832715974481203121946751686379343096189615107330065552421485195201762858595091051839472502863871632494167613804996319791441870254302706758495192008837915169401581740046711477877201459644461175204059453504764721807975761111720846273639279600339670470037613374509553184150073796412605047923251661354841291884211340823015473304754067072818763503617332908005951896325207071673904547777129682265206225651439919376804400292380903112437912614776255964694221981375146967079446870358004392507659451618379811859392049544036114915310782251072691486979809240946772142727012404377187409216756613634938900451232351668146089322400697993176017805338191849981933008410985993938760292601390911414526003720284872132411955424282101831204216104467404621635336900583664606591156298764745525068145003932941404131495400677602951005962253022823003631473824681059648442441324864573137437595096416168048024129351876204668135636877532814675538798871771836512893947195335061885003267607354388673368002074387849657014576090349857571243045102038730494854256702479339322809110526041538528994849203991091946129912491633289917998094380337879522093131466946149705939664152375949285890960489916121944989986384837022486672249148924678410206183364627416969576307632480235587975245253737035433882960862753427740016333434055083537048507374544819754722228975281083020898682633020285259923084168054539687911418297629988964576482765287504562854924265165217750799516259669229114977788962356670956627138482018191348321687995863652637620978285070099337294396784639879024914514222742527006363942327998483976739987154418554201562244154926653014515504685489258620276085761837129763358761215382565129633538141663949516556000264159186554850057052611431952919918807954522394649627635630178580896692226406235382898535867595990647008385687123810329591926494846250768992258419305480763620215089022149220528069842018350840586938493815498909445461977893029113576516775406232278298314033473276603952231603422824717528181818844304880921321933550869873395861276073670866652375555675803171490108477320096424318780070008797346032906278943553743564448851907191616455141155761939399690767415156402826543664026760095087523945507341556135867933066031744720924446513532366647649735400851967040771103640538150073486891798364049570606189535005089840913826869535090066783324472578712196604415284924840041850932811908963634175739897166596000759487800619164094854338758520657116541072260996288150123144377944008749301944744330784388995701842710004808305012177123560622895076269042856800047718893158089358515593863176652948089031267747029662545110861548958395087796755464137944895960527975209874813839762578592105756284401759349324162148339565350189196811389091843795734703269406342890087805846940352453479398080674273236297887100867175802531561302356064878709259865288416350972529537091114317204887747405539054009425375424119317944175137064689643861517718849867010341532542385911089624710885385808688837777258648564145934262121086647588489260031762345960769508849149662444156604419552086811989770240.0) | |
| function last | |
| :real = | |
| (1189731495357231765021263853030970205169063322294624200440323733891737005522970722616410290336528882853545697807495577314427443153670288434198125573853743678673593200706973263201915918282961524365529510646791086614311790632169778838896134786560600399148753433211454911160088679845154866512852340149773037600009125479393966223151383622417838542743917838138717805889487540575168226347659235576974805113725649020884855222494791399377585026011773549180099796226026859508558883608159846900235645132346594476384939859276456284579661772930407806609229102715046085388087959327781622986827547830768080040150694942303411728957777100335714010559775242124057347007386251660110828379119623008469277200965153500208474470792443848545912886723000619085126472111951361467527633519562927597957250278002980795904193139603021470997035276467445530922022679656280991498232083329641241038509239184734786121921697210543484287048353408113042573002216421348917347174234800714880751002064390517234247656004721768096486107994943415703476320643558624207443504424380566136017608837478165389027809576975977286860071487028287955567141404632615832623602762896316173978484254486860609948270867968048078702511858930838546584223040908805996294594586201903766048446790926002225410530775901065760671347200125846406957030257138960983757998926954553052368560758683179223113639519468850880771872104705203957587480013143131444254943919940175753169339392366881856189129931729104252921236835159922322050998001677102784035360140829296398115122877768135706045789343535451696539561254048846447169786893211671087229088082778350518228857646062218739702851655083720992349483334435228984751232753726636066213902281264706234075352071724058665079518217303463782631353393706774901950197841690441824738063162828586857741432581165364040218402724913393320949219498422442730427019873044536620350262386957804682003601447291997123095530057206141866974852846856186514832715974481203121946751686379343096189615107330065552421485195201762858595091051839472502863871632494167613804996319791441870254302706758495192008837915169401581740046711477877201459644461175204059453504764721807975761111720846273639279600339670470037613374509553184150073796412605047923251661354841291884211340823015473304754067072818763503617332908005951896325207071673904547777129682265206225651439919376804400292380903112437912614776255964694221981375146967079446870358004392507659451618379811859392049544036114915310782251072691486979809240946772142727012404377187409216756613634938900451232351668146089322400697993176017805338191849981933008410985993938760292601390911414526003720284872132411955424282101831204216104467404621635336900583664606591156298764745525068145003932941404131495400677602951005962253022823003631473824681059648442441324864573137437595096416168048024129351876204668135636877532814675538798871771836512893947195335061885003267607354388673368002074387849657014576090349857571243045102038730494854256702479339322809110526041538528994849203991091946129912491633289917998094380337879522093131466946149705939664152375949285890960489916121944989986384837022486672249148924678410206183364627416969576307632480235587975245253737035433882960862753427740016333434055083537048507374544819754722228975281083020898682633020285259923084168054539687911418297629988964576482765287504562854924265165217750799516259669229114977788962356670956627138482018191348321687995863652637620978285070099337294396784639879024914514222742527006363942327998483976739987154418554201562244154926653014515504685489258620276085761837129763358761215382565129633538141663949516556000264159186554850057052611431952919918807954522394649627635630178580896692226406235382898535867595990647008385687123810329591926494846250768992258419305480763620215089022149220528069842018350840586938493815498909445461977893029113576516775406232278298314033473276603952231603422824717528181818844304880921321933550869873395861276073670866652375555675803171490108477320096424318780070008797346032906278943553743564448851907191616455141155761939399690767415156402826543664026760095087523945507341556135867933066031744720924446513532366647649735400851967040771103640538150073486891798364049570606189535005089840913826869535090066783324472578712196604415284924840041850932811908963634175739897166596000759487800619164094854338758520657116541072260996288150123144377944008749301944744330784388995701842710004808305012177123560622895076269042856800047718893158089358515593863176652948089031267747029662545110861548958395087796755464137944895960527975209874813839762578592105756284401759349324162148339565350189196811389091843795734703269406342890087805846940352453479398080674273236297887100867175802531561302356064878709259865288416350972529537091114317204887747405539054009425375424119317944175137064689643861517718849867010341532542385911089624710885385808688837777258648564145934262121086647588489260031762345960769508849149662444156604419552086811989770240.0) | |
| predicate in_range | |
| (x : real) = | |
| ( ( first <=. x ) /\ ( x <=. last ) ) | |
| clone export "ada__model".Static_Floating_Point with | |
| type t = long_long_float, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "character", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__character | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type character "bounded_type" | |
| function first | |
| :int = | |
| 0 | |
| function last | |
| :int = | |
| 255 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = character, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "wide_character", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__wide_character | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type wide_character "bounded_type" | |
| function first | |
| :int = | |
| 0 | |
| function last | |
| :int = | |
| 65535 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = wide_character, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "wide_wide_character", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__wide_wide_character | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type wide_wide_character "bounded_type" | |
| function first | |
| :int = | |
| 0 | |
| function last | |
| :int = | |
| 2147483647 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = wide_wide_character, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "string", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__string | |
| use import "_gnatprove_standard".Main | |
| use Standard__positive | |
| use Standard__character | |
| use Standard__integer | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| use "_gnatprove_standard".Array__1 | |
| clone export "ada__model".Unconstr_Array with | |
| type component_type = Standard__character.character, | |
| type base_type = Standard__integer.integer, | |
| function to_int = Standard__integer.to_int, | |
| predicate in_range_base = Standard__integer.in_range, | |
| predicate in_range = Standard__positive.in_range | |
| type string = | |
| __t | |
| function to_string | |
| (x : __image) :string | |
| function from_string | |
| (x : string) :__image | |
| clone export "ada__model".Array_Comparison_Axiom with | |
| type component_type = Standard__character.character, | |
| function to_int = Standard__character.to_int | |
| end | |
| (* Module for axiomatizing type "wide_string", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__wide_string | |
| use import "_gnatprove_standard".Main | |
| use Standard__positive | |
| use Standard__wide_character | |
| use Standard__integer | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| use "_gnatprove_standard".Array__1 | |
| clone export "ada__model".Unconstr_Array with | |
| type component_type = Standard__wide_character.wide_character, | |
| type base_type = Standard__integer.integer, | |
| function to_int = Standard__integer.to_int, | |
| predicate in_range_base = Standard__integer.in_range, | |
| predicate in_range = Standard__positive.in_range | |
| type wide_string = | |
| __t | |
| clone export "ada__model".Array_Comparison_Axiom with | |
| type component_type = Standard__wide_character.wide_character, | |
| function to_int = Standard__wide_character.to_int | |
| end | |
| (* Module for axiomatizing type "wide_wide_string", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__wide_wide_string | |
| use import "_gnatprove_standard".Main | |
| use Standard__positive | |
| use Standard__wide_wide_character | |
| use Standard__integer | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| use "_gnatprove_standard".Array__1 | |
| clone export "ada__model".Unconstr_Array with | |
| type component_type = Standard__wide_wide_character.wide_wide_character, | |
| type base_type = Standard__integer.integer, | |
| function to_int = Standard__integer.to_int, | |
| predicate in_range_base = Standard__integer.in_range, | |
| predicate in_range = Standard__positive.in_range | |
| type wide_wide_string = | |
| __t | |
| clone export "ada__model".Array_Comparison_Axiom with | |
| type component_type = Standard__wide_wide_character.wide_wide_character, | |
| function to_int = Standard__wide_wide_character.to_int | |
| end | |
| (* Module for axiomatizing type "duration", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__duration | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type duration "bounded_type" | |
| function first | |
| :__fixed = | |
| ( -9223372036854775808 ) | |
| function last | |
| :__fixed = | |
| 9223372036854775807 | |
| function inv_small | |
| :__fixed = | |
| 1000000000 | |
| predicate in_range | |
| (x : __fixed) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Fixed_Point with | |
| type t = duration, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range, | |
| function inv_small = inv_small | |
| end | |
| (* Module for axiomatizing type "integer_8", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__integer_8 | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type integer_8 "bounded_type" | |
| function first | |
| :int = | |
| ( -128 ) | |
| function last | |
| :int = | |
| 127 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = integer_8, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "integer_16", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__integer_16 | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type integer_16 "bounded_type" | |
| function first | |
| :int = | |
| ( -32768 ) | |
| function last | |
| :int = | |
| 32767 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = integer_16, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "integer_32", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__integer_32 | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type integer_32 "bounded_type" | |
| function first | |
| :int = | |
| ( -2147483648 ) | |
| function last | |
| :int = | |
| 2147483647 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = integer_32, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "integer_64", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__integer_64 | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type integer_64 "bounded_type" | |
| function first | |
| :int = | |
| ( -9223372036854775808 ) | |
| function last | |
| :int = | |
| 9223372036854775807 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = integer_64, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "universal_integer", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__universal_integer | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| type universal_integer "bounded_type" | |
| function first | |
| :int = | |
| ( -9223372036854775808 ) | |
| function last | |
| :int = | |
| 9223372036854775807 | |
| predicate in_range | |
| (x : int) = | |
| ( ( first <= x ) /\ ( x <= last ) ) | |
| clone export "ada__model".Static_Discrete with | |
| type t = universal_integer, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for axiomatizing type "universal_real", created in Gnat2Why.Types.Translate_Type *) | |
| module Standard__universal_real | |
| use import "_gnatprove_standard".Main | |
| use "_gnatprove_standard".Floating | |
| use import "real".RealInfix | |
| type universal_real "bounded_type" | |
| function first | |
| :real = | |
| (-.1189731495357231765021263853030970205169063322294624200440323733891737005522970722616410290336528882853545697807495577314427443153670288434198125573853743678673593200706973263201915918282961524365529510646791086614311790632169778838896134786560600399148753433211454911160088679845154866512852340149773037600009125479393966223151383622417838542743917838138717805889487540575168226347659235576974805113725649020884855222494791399377585026011773549180099796226026859508558883608159846900235645132346594476384939859276456284579661772930407806609229102715046085388087959327781622986827547830768080040150694942303411728957777100335714010559775242124057347007386251660110828379119623008469277200965153500208474470792443848545912886723000619085126472111951361467527633519562927597957250278002980795904193139603021470997035276467445530922022679656280991498232083329641241038509239184734786121921697210543484287048353408113042573002216421348917347174234800714880751002064390517234247656004721768096486107994943415703476320643558624207443504424380566136017608837478165389027809576975977286860071487028287955567141404632615832623602762896316173978484254486860609948270867968048078702511858930838546584223040908805996294594586201903766048446790926002225410530775901065760671347200125846406957030257138960983757998926954553052368560758683179223113639519468850880771872104705203957587480013143131444254943919940175753169339392366881856189129931729104252921236835159922322050998001677102784035360140829296398115122877768135706045789343535451696539561254048846447169786893211671087229088082778350518228857646062218739702851655083720992349483334435228984751232753726636066213902281264706234075352071724058665079518217303463782631353393706774901950197841690441824738063162828586857741432581165364040218402724913393320949219498422442730427019873044536620350262386957804682003601447291997123095530057206141866974852846856186514832715974481203121946751686379343096189615107330065552421485195201762858595091051839472502863871632494167613804996319791441870254302706758495192008837915169401581740046711477877201459644461175204059453504764721807975761111720846273639279600339670470037613374509553184150073796412605047923251661354841291884211340823015473304754067072818763503617332908005951896325207071673904547777129682265206225651439919376804400292380903112437912614776255964694221981375146967079446870358004392507659451618379811859392049544036114915310782251072691486979809240946772142727012404377187409216756613634938900451232351668146089322400697993176017805338191849981933008410985993938760292601390911414526003720284872132411955424282101831204216104467404621635336900583664606591156298764745525068145003932941404131495400677602951005962253022823003631473824681059648442441324864573137437595096416168048024129351876204668135636877532814675538798871771836512893947195335061885003267607354388673368002074387849657014576090349857571243045102038730494854256702479339322809110526041538528994849203991091946129912491633289917998094380337879522093131466946149705939664152375949285890960489916121944989986384837022486672249148924678410206183364627416969576307632480235587975245253737035433882960862753427740016333434055083537048507374544819754722228975281083020898682633020285259923084168054539687911418297629988964576482765287504562854924265165217750799516259669229114977788962356670956627138482018191348321687995863652637620978285070099337294396784639879024914514222742527006363942327998483976739987154418554201562244154926653014515504685489258620276085761837129763358761215382565129633538141663949516556000264159186554850057052611431952919918807954522394649627635630178580896692226406235382898535867595990647008385687123810329591926494846250768992258419305480763620215089022149220528069842018350840586938493815498909445461977893029113576516775406232278298314033473276603952231603422824717528181818844304880921321933550869873395861276073670866652375555675803171490108477320096424318780070008797346032906278943553743564448851907191616455141155761939399690767415156402826543664026760095087523945507341556135867933066031744720924446513532366647649735400851967040771103640538150073486891798364049570606189535005089840913826869535090066783324472578712196604415284924840041850932811908963634175739897166596000759487800619164094854338758520657116541072260996288150123144377944008749301944744330784388995701842710004808305012177123560622895076269042856800047718893158089358515593863176652948089031267747029662545110861548958395087796755464137944895960527975209874813839762578592105756284401759349324162148339565350189196811389091843795734703269406342890087805846940352453479398080674273236297887100867175802531561302356064878709259865288416350972529537091114317204887747405539054009425375424119317944175137064689643861517718849867010341532542385911089624710885385808688837777258648564145934262121086647588489260031762345960769508849149662444156604419552086811989770240.0) | |
| function last | |
| :real = | |
| (1189731495357231765021263853030970205169063322294624200440323733891737005522970722616410290336528882853545697807495577314427443153670288434198125573853743678673593200706973263201915918282961524365529510646791086614311790632169778838896134786560600399148753433211454911160088679845154866512852340149773037600009125479393966223151383622417838542743917838138717805889487540575168226347659235576974805113725649020884855222494791399377585026011773549180099796226026859508558883608159846900235645132346594476384939859276456284579661772930407806609229102715046085388087959327781622986827547830768080040150694942303411728957777100335714010559775242124057347007386251660110828379119623008469277200965153500208474470792443848545912886723000619085126472111951361467527633519562927597957250278002980795904193139603021470997035276467445530922022679656280991498232083329641241038509239184734786121921697210543484287048353408113042573002216421348917347174234800714880751002064390517234247656004721768096486107994943415703476320643558624207443504424380566136017608837478165389027809576975977286860071487028287955567141404632615832623602762896316173978484254486860609948270867968048078702511858930838546584223040908805996294594586201903766048446790926002225410530775901065760671347200125846406957030257138960983757998926954553052368560758683179223113639519468850880771872104705203957587480013143131444254943919940175753169339392366881856189129931729104252921236835159922322050998001677102784035360140829296398115122877768135706045789343535451696539561254048846447169786893211671087229088082778350518228857646062218739702851655083720992349483334435228984751232753726636066213902281264706234075352071724058665079518217303463782631353393706774901950197841690441824738063162828586857741432581165364040218402724913393320949219498422442730427019873044536620350262386957804682003601447291997123095530057206141866974852846856186514832715974481203121946751686379343096189615107330065552421485195201762858595091051839472502863871632494167613804996319791441870254302706758495192008837915169401581740046711477877201459644461175204059453504764721807975761111720846273639279600339670470037613374509553184150073796412605047923251661354841291884211340823015473304754067072818763503617332908005951896325207071673904547777129682265206225651439919376804400292380903112437912614776255964694221981375146967079446870358004392507659451618379811859392049544036114915310782251072691486979809240946772142727012404377187409216756613634938900451232351668146089322400697993176017805338191849981933008410985993938760292601390911414526003720284872132411955424282101831204216104467404621635336900583664606591156298764745525068145003932941404131495400677602951005962253022823003631473824681059648442441324864573137437595096416168048024129351876204668135636877532814675538798871771836512893947195335061885003267607354388673368002074387849657014576090349857571243045102038730494854256702479339322809110526041538528994849203991091946129912491633289917998094380337879522093131466946149705939664152375949285890960489916121944989986384837022486672249148924678410206183364627416969576307632480235587975245253737035433882960862753427740016333434055083537048507374544819754722228975281083020898682633020285259923084168054539687911418297629988964576482765287504562854924265165217750799516259669229114977788962356670956627138482018191348321687995863652637620978285070099337294396784639879024914514222742527006363942327998483976739987154418554201562244154926653014515504685489258620276085761837129763358761215382565129633538141663949516556000264159186554850057052611431952919918807954522394649627635630178580896692226406235382898535867595990647008385687123810329591926494846250768992258419305480763620215089022149220528069842018350840586938493815498909445461977893029113576516775406232278298314033473276603952231603422824717528181818844304880921321933550869873395861276073670866652375555675803171490108477320096424318780070008797346032906278943553743564448851907191616455141155761939399690767415156402826543664026760095087523945507341556135867933066031744720924446513532366647649735400851967040771103640538150073486891798364049570606189535005089840913826869535090066783324472578712196604415284924840041850932811908963634175739897166596000759487800619164094854338758520657116541072260996288150123144377944008749301944744330784388995701842710004808305012177123560622895076269042856800047718893158089358515593863176652948089031267747029662545110861548958395087796755464137944895960527975209874813839762578592105756284401759349324162148339565350189196811389091843795734703269406342890087805846940352453479398080674273236297887100867175802531561302356064878709259865288416350972529537091114317204887747405539054009425375424119317944175137064689643861517718849867010341532542385911089624710885385808688837777258648564145934262121086647588489260031762345960769508849149662444156604419552086811989770240.0) | |
| predicate in_range | |
| (x : real) = | |
| ( ( first <=. x ) /\ ( x <=. last ) ) | |
| clone export "ada__model".Static_Floating_Point with | |
| type t = universal_real, | |
| function first = first, | |
| function last = last, | |
| predicate in_range = in_range | |
| end | |
| (* Module for defining the constant "x" defined at test1.ads:6, created in Gnat2Why.Decls.Translate_Constant *) | |
| module Test1__fact__x | |
| use import "_gnatprove_standard".Main | |
| use Standard__integer | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| function x | |
| :Standard__integer.integer | |
| end | |
| (* Module giving an empty axiom for the entity "x" defined at test1.ads:6, created in Gnat2Why.Driver.Translate_Entity.Generate_Empty_Axiom_Theory *) | |
| module Test1__fact__x__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module for declaring a program function (and possibly a logic function) for "fact" defined at test1.ads:6, created in Gnat2Why.Subprograms.Translate_Subprogram_Spec *) | |
| module Test1__fact | |
| use import "_gnatprove_standard".Main | |
| use Standard__integer | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| function fact | |
| (x : int) :Standard__integer.integer | |
| val fact | |
| (x : int) :Standard__integer.integer | |
| requires { true } | |
| ensures { ( result = (fact x) ) } | |
| end | |
| (* Module giving a defining axiom for the expression function "fact" defined at test1.ads:6, created in Gnat2Why.Subprograms.Translate_Expression_Function_Body *) | |
| module Test1__fact__axiom | |
| use import "_gnatprove_standard".Main | |
| use Standard__integer | |
| use Test1__fact | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| axiom def_axiom : | |
| (forall x : int [(Test1__fact.fact x)]. | |
| ( (Standard__integer.in_range x) -> ( (Test1__fact.fact x) = (if (( x > 0 )) then ( | |
| (Standard__integer.of_int ( x * (Standard__integer.to_int (Test1__fact.fact ( x - 1 ))) ))) else ( | |
| (Standard__integer.of_int 1))) ) )) | |
| end | |
| (* Module giving axioms for the type entity "short_short_integer", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__short_short_integer__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "short_integer", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__short_integer__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "integer", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__integer__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "long_integer", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__long_integer__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "long_long_integer", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__long_long_integer__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "natural", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__natural__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "positive", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__positive__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "short_float", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__short_float__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "float", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__float__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "long_float", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__long_float__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "long_long_float", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__long_long_float__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "character", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__character__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "wide_character", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__wide_character__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "wide_wide_character", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__wide_wide_character__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "string", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__string__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "wide_string", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__wide_string__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "wide_wide_string", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__wide_wide_string__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "duration", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__duration__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "integer_8", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__integer_8__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "integer_16", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__integer_16__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "integer_32", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__integer_32__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "integer_64", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__integer_64__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "universal_integer", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__universal_integer__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module giving axioms for the type entity "universal_real", created in Gnat2Why.Types.Generate_Type_Completion *) | |
| module Standard__universal_real__axiom | |
| use import "_gnatprove_standard".Main | |
| end | |
| (* Module for checking absence of run-time errors and package initial condition on package elaboration of "test1" defined at test1.ads:2, created in Gnat2Why.Subprograms.Generate_VCs_For_Package_Elaboration *) | |
| module Test1__package_def | |
| use import "_gnatprove_standard".Main | |
| let def "GP_Subp:test1.ads:2" "GP_Pretty_Ada:test1" "W:diverges:N" | |
| (__void_param : unit) | |
| requires { true } | |
| ensures { true } | |
| = | |
| () | |
| end | |
| (* Module for checking contracts and absence of run-time errors in subprogram "fact" defined at test1.ads:6, created in Gnat2Why.Subprograms.Generate_VCs_For_Subprogram *) | |
| module Test1__fact__subprogram_def | |
| use import "int".Int | |
| use import "_gnatprove_standard".Main | |
| use Standard__integer | |
| use Standard__integer__axiom | |
| use Standard__integer | |
| use Standard__integer__axiom | |
| use Test1__fact | |
| use Test1__fact__axiom | |
| use Test1__fact__x | |
| use Test1__fact__x__axiom | |
| use "_gnatprove_standard".Integer | |
| use import "int".Int | |
| val test1__fact__result "\"GP_Ada_Name:fact'Result\"" : ref Standard__integer.integer | |
| let def "W:diverges:N" "GP_Subp:test1.ads:6" "GP_Pretty_Ada:test1.fact" | |
| (__void_param : unit) | |
| requires { true } | |
| ensures { true } | |
| = | |
| ( ( abstract ensures {true}(___ignore(True)) end ; | |
| (any unit | |
| requires {true} | |
| ensures {true} | |
| ) ); | |
| ( try | |
| ( ( "GP_Sloc:test1.ads:7:7" ( test1__fact__result := ( (if (( (Standard__integer.to_int(Test1__fact__x.x)) > 0 )) then ( | |
| (Standard__integer.of_int(( "GP_Reason:VC_OVERFLOW_CHECK" "keep_on_simp" "GP_Sloc_VC:test1.ads:8:12" (Standard__integer.range_check_(( (Standard__integer.to_int(Test1__fact__x.x)) * (Standard__integer.to_int((Test1__fact.fact(( "GP_Reason:VC_OVERFLOW_CHECK" "GP_Sloc_VC:test1.ads:8:22" "keep_on_simp" (Standard__integer.range_check_(( (Standard__integer.to_int(Test1__fact__x.x)) - 1 ))) ))))) ))) )))) else ( | |
| (Standard__integer.of_int(1)))) ); | |
| raise Return__exc ) ); | |
| raise Return__exc ) | |
| with | |
| Return__exc -> () | |
| end; | |
| abstract ensures {true}(___ignore(True)) end ; | |
| !test1__fact__result ) ) | |
| end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| pragma Annotate (GNATprove, External_Axiomatization); | |
| package test2 | |
| with Pure, SPARK_Mode | |
| is | |
| function fact (x : Integer) return Positive is -- change to Positive | |
| (if x /= 0 then -- change from ">" to "/=" | |
| x * fact (x - 1) -- overflow check might fail, range check might fail | |
| else | |
| 1); | |
| end test2; | |
| -- $ gnatprove -Ptests --mode=all test2.ads | |
| -- Phase 1 of 3: frame condition computation ... | |
| -- Phase 2 of 3: analysis and translation to intermediate language ... | |
| -- Phase 3 of 3: generation and proof of VCs ... | |
| -- analyzing test2, 0 checks | |
| -- analyzing test2.fact, 3 checks | |
| -- test2.ads:8:12: warning: overflow check might fail | |
| -- test2.ads:8:12: warning: range check might fail | |
| -- test2.ads:8:22: warning: overflow check might fail | |
| -- gprbuild: *** compilation phase failed | |
| -- gnatprove: error during generation and proof of VCs, aborting. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| pragma Annotate (GNATprove, External_Axiomatization); | |
| package test3 | |
| with Pure, SPARK_Mode | |
| is | |
| subtype Small_Natural is Integer range 0 .. 10; | |
| subtype Small_Result is Integer range 1 .. 3628800; | |
| function fact (x : Small_Natural) return Small_Result is | |
| (if x > 0 then | |
| x * fact (x - 1) | |
| else | |
| 1) | |
| with Contract_Cases => | |
| (x <= 1 => fact'Result = 1, | |
| x = 2 => fact'Result = 2, | |
| x = 3 => fact'Result = 6, | |
| x = 4 => fact'Result = 24, | |
| x = 5 => fact'Result = 120, | |
| x = 6 => fact'Result = 720, | |
| x = 7 => fact'Result = 5040, | |
| x = 8 => fact'Result = 40320, | |
| x = 9 => fact'Result = 362880, | |
| x = 10 => fact'Result = 3628800); | |
| end test3; | |
| -- $ gnatprove -Ptests --mode=all test3.ads | |
| -- Phase 1 of 3: frame condition computation ... | |
| -- Phase 2 of 3: analysis and translation to intermediate language ... | |
| -- Phase 3 of 3: generation and proof of VCs ... | |
| -- analyzing test3, 0 checks | |
| -- analyzing test3.fact, 15 checks | |
| -- Summary logged in /Users/yt/projects/experimental/ada/spark/gnatprove/gnatprove.out |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| project tests is | |
| for Source_Dirs use ("."); | |
| end tests; |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment